package gui;

import java.awt.BorderLayout;
import java.awt.Dimension;
import java.awt.EventQueue;
import java.awt.GridLayout;
import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.io.BufferedReader;
import java.io.IOException;
import java.nio.charset.Charset;
import java.nio.file.Files;
import java.util.ArrayList;
import java.util.Collections;
import java.util.Map;

import javax.swing.DefaultListModel;
import javax.swing.JButton;
import javax.swing.JCheckBox;
import javax.swing.JFileChooser;
import javax.swing.JFrame;
import javax.swing.JLabel;
import javax.swing.JList;
import javax.swing.JPanel;
import javax.swing.JScrollPane;
import javax.swing.JTextField;
import javax.swing.ListSelectionModel;
import javax.swing.border.EtchedBorder;
import javax.swing.filechooser.FileNameExtensionFilter;

import minsat.BindingsAndBound;
import minsat.Clause;
import minsat.Formula;
import minsat.MinSatz;

/**
 * Java Swing GUI allowing easy editing of formulas and instantiation of the MinSatz and optimal
 * solvers.
 */
public class MainGui
{
  private JFrame frmMinsatzSolver;
  private JTextField clauseEntry;
  private JTextField weightEntry;
  private Formula formula;
  private JList<String> minSatzResultsField;
  private JList<String> optimalResultsField;

  final DefaultListModel<Clause> clauseListModel = new DefaultListModel<Clause>();
  final DefaultListModel<String> minSatzListModel = new DefaultListModel<String>();
  final DefaultListModel<String> optimalListModel = new DefaultListModel<String>();
  final JLabel lblOptimalScore = new JLabel("Score:");
  final JLabel lblMinSatzScore = new JLabel("Score: ");

  /**
   * Launch the application.
   */
  public static void main(String[] args)
  {
    EventQueue.invokeLater(new Runnable() {
      public void run()
      {
        try {
          MainGui window = new MainGui();
          window.frmMinsatzSolver.setVisible(true);
        }
        catch (Exception e) {
          e.printStackTrace();
        }
      }
    });
  }

  /**
   * Create the application.
   */
  public MainGui()
  {
    initialize();
  }

  /**
   * Initialize the contents of the frame.
   */
  private void initialize()
  {
    formula = new Formula();

    frmMinsatzSolver = new JFrame();
    frmMinsatzSolver.setTitle("MinSatz Solver");
    frmMinsatzSolver.setBounds(100, 100, 593, 352);
    frmMinsatzSolver.setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE);
    frmMinsatzSolver.getContentPane().setLayout(new BorderLayout(0, 0));

    JPanel newLiteralPanel = new JPanel();
    frmMinsatzSolver.getContentPane().add(newLiteralPanel, BorderLayout.NORTH);

    JLabel lblNewLabel = new JLabel("Enter new clause:");
    newLiteralPanel.add(lblNewLabel);

    clauseEntry = new JTextField();
    newLiteralPanel.add(clauseEntry);
    clauseEntry.setColumns(10);

    JLabel lblWeight = new JLabel("Weight:");
    newLiteralPanel.add(lblWeight);

    weightEntry = new JTextField();
    weightEntry.setPreferredSize(new Dimension(4, 20));
    newLiteralPanel.add(weightEntry);
    weightEntry.setColumns(10);

    final JCheckBox hardCheckBox = new JCheckBox("Hard?");
    hardCheckBox.addActionListener(new ActionListener() {
      public void actionPerformed(ActionEvent e)
      {
        weightEntry.setEditable(!hardCheckBox.isSelected());
      }
    });
    newLiteralPanel.add(hardCheckBox);

    JButton btnAdd = new JButton("Add");
    btnAdd.addActionListener(new ActionListener() {
      public void actionPerformed(ActionEvent e)
      {
        clearResults();
        Clause c =
            new Clause(clauseEntry.getText(), ((hardCheckBox.isSelected())
                ? Double.POSITIVE_INFINITY : Double.parseDouble(weightEntry.getText())));
        formula.addClause(c);

        clauseListModel.addElement(c);
        clauseEntry.setText("");
        weightEntry.setText("");
      }
    });
    newLiteralPanel.add(btnAdd);

    JPanel controlPanel = new JPanel();
    frmMinsatzSolver.getContentPane().add(controlPanel, BorderLayout.SOUTH);

    JPanel mainPanel = new JPanel();
    frmMinsatzSolver.getContentPane().add(mainPanel, BorderLayout.CENTER);
    mainPanel.setLayout(new GridLayout(0, 2, 0, 0));

    JPanel leftPanel = new JPanel();
    leftPanel.setBorder(new EtchedBorder(EtchedBorder.LOWERED, null, null));
    leftPanel.setName("");
    mainPanel.add(leftPanel);
    leftPanel.setLayout(new BorderLayout(0, 0));

    JScrollPane scrollPane = new JScrollPane();
    leftPanel.add(scrollPane);

    JList<Clause> clauseList = new JList<Clause>();
    clauseList.setModel(clauseListModel);
    clauseList.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
    scrollPane.setViewportView(clauseList);

    JLabel lblClauses = new JLabel("Clauses:");
    leftPanel.add(lblClauses, BorderLayout.NORTH);

    JPanel rightPanel = new JPanel();
    mainPanel.add(rightPanel);
    rightPanel.setLayout(new GridLayout(2, 1, 0, 0));

    JPanel minSatzResultPanel = new JPanel();
    minSatzResultPanel.setBorder(new EtchedBorder(EtchedBorder.LOWERED, null, null));
    rightPanel.add(minSatzResultPanel);
    minSatzResultPanel.setLayout(new BorderLayout(0, 0));

    JLabel lblMinsatzResults = new JLabel("MinSatz results:");
    minSatzResultPanel.add(lblMinsatzResults, BorderLayout.NORTH);

    minSatzResultPanel.add(lblMinSatzScore, BorderLayout.SOUTH);

    minSatzResultsField = new JList<String>();
    minSatzResultsField.setModel(minSatzListModel);
    JScrollPane minSatzScrollPane = new JScrollPane();
    minSatzResultPanel.add(minSatzScrollPane, BorderLayout.CENTER);
    minSatzScrollPane.setViewportView(minSatzResultsField);

    JPanel optimalResultPanel = new JPanel();
    optimalResultPanel.setBorder(new EtchedBorder(EtchedBorder.LOWERED, null, null));
    rightPanel.add(optimalResultPanel);
    optimalResultPanel.setLayout(new BorderLayout(0, 0));

    JLabel lblOptimalResults = new JLabel("Optimal Results:");
    optimalResultPanel.add(lblOptimalResults, BorderLayout.NORTH);

    optimalResultsField = new JList<String>();
    optimalResultsField.setModel(optimalListModel);
    JScrollPane optimalScrollPane = new JScrollPane();
    optimalResultPanel.add(optimalScrollPane, BorderLayout.CENTER);
    optimalScrollPane.setViewportView(optimalResultsField);

    optimalResultPanel.add(lblOptimalScore, BorderLayout.SOUTH);

    JButton btnSolveOptimal = new JButton("Solve Optimal");
    btnSolveOptimal.addActionListener(new ActionListener() {
      public void actionPerformed(ActionEvent e)
      {
        clearOptimal();
        long startTime = System.currentTimeMillis();
        Map<String, Boolean> optimalBindings = MinSatz.optimalSat(new Formula(formula));
        long stopTime = System.currentTimeMillis();
        java.util.List<String> keys = new ArrayList<String>(optimalBindings.keySet());
        Collections.sort(keys);
        for (String s : keys)
          optimalListModel.addElement(s + " <-- " + optimalBindings.get(s));
        double score = new Formula(formula).evaluate(optimalBindings);
        long elapsedTime = stopTime - startTime;
        lblOptimalScore.setText("Score: " + score + "    Time (ms): " + elapsedTime);
      }
    });
    controlPanel.add(btnSolveOptimal);

    JButton btnSolveMinsatz = new JButton("Solve MinSatz");
    btnSolveMinsatz.addActionListener(new ActionListener() {
      public void actionPerformed(ActionEvent e)
      {
        clearMinSatz();
        BindingsAndBound lowerBound = new BindingsAndBound();
        long startTime = System.currentTimeMillis();
        lowerBound = MinSatz.runMinSatz(new Formula(formula), lowerBound, null);
        long stopTime = System.currentTimeMillis();
        Map<String, Boolean> optimalBindings = MinSatz.convertToMap(lowerBound);
        java.util.List<String> keys = new ArrayList<String>(optimalBindings.keySet());
        Collections.sort(keys);
        for (String s : keys)
          minSatzListModel.addElement(s + " <-- " + optimalBindings.get(s));

        long elapsedTime = stopTime - startTime;
        lblMinSatzScore.setText("Score: " + lowerBound.bound + "    Time (ms): " + elapsedTime);
      }
    });
    controlPanel.add(btnSolveMinsatz);

    JButton btnClearAll = new JButton("Clear All");
    btnClearAll.addActionListener(new ActionListener() {
      public void actionPerformed(ActionEvent e)
      {
        clearAll();
      }
    });
    controlPanel.add(btnClearAll);

    JButton btnLoad = new JButton("Load");
    btnLoad.addActionListener(new ActionListener() {
      public void actionPerformed(ActionEvent e)
      {
        JFileChooser chooser = new JFileChooser();
        FileNameExtensionFilter filter = new FileNameExtensionFilter("Text files", "txt");
        chooser.setFileFilter(filter);
        int returnVal = chooser.showOpenDialog(frmMinsatzSolver);
        if (returnVal == JFileChooser.APPROVE_OPTION) {
          clearAll();

          Charset charset = Charset.forName("US-ASCII");
          try (BufferedReader reader =
              Files.newBufferedReader(chooser.getSelectedFile().toPath(), charset)) {
            String line = null;
            formula = new Formula();
            while ((line = reader.readLine()) != null) {
              String weight = line.substring(0, line.indexOf(" "));
              Double w;
              if (weight.equals("inf"))
                w = Double.POSITIVE_INFINITY;
              else
                w = Double.parseDouble(weight);
              Clause c = new Clause(line.substring(line.indexOf(" ") + 1), w);
              formula.addClause(c);
              clauseListModel.addElement(c);
            }
          }
          catch (IOException x) {
            System.err.format("IOException: %s%n", x);
          }
        }
      }
    });
    controlPanel.add(btnLoad);
  }

  private void clearAll()
  {
    clauseListModel.clear();
    formula = new Formula();
    clearResults();
  }

  private void clearResults()
  {
    clearMinSatz();
    clearOptimal();
  }

  private void clearMinSatz()
  {
    minSatzListModel.clear();
    lblMinSatzScore.setText("Score: ");
  }

  private void clearOptimal()
  {
    optimalListModel.clear();
    lblOptimalScore.setText("Score: ");
  }
}
